Nuprl Definition : d-single-pre
11,40
postcript
pdf
@
i
(with ds:
ds
action
a
:
T
precondition
a
is
P
s)(
j
)
== if eqof(IdDeq)(
j
,
i
) then (precondition
a
:Outcome(
T
) is
P
:State(
ds
) -> Bool) else fi
latex
Definitions
,
(precondition
a
:Outcome(
p
) is
P
:State(
ds
) -> Bool)
,
IdDeq
,
eqof(
d
)
,
if
b
then
t
else
f
fi
FDL editor aliases
d-single-pre
origin